“Taking the principle of excluded middle from the mathematician would be the same, say, as proscribing the telescope to the astronomer or to the boxer the use of his fists” - David Hilbert
If we stop with the rules presented so far, we have what is called Constructive Propositional Logic (also known as Intuitionistic Propositional Logic).
The rules are sound (in that the rules will only let us prove consequences of our assumptions that are logically entailed by those assumptions), but they are not complete (in that there are “true” entailments that cannot be proved with the constructive introduction and elimination rules).
For the system to be complete, we need one more rule. In fact, there are many choices for what that one rule should be; we present the three most common choices here. The three rules are equivalent, in that any one of the rules makes the system complete. We show all three, because sometimes one is easier to use than the others, depending on what you are trying to prove.
First, we have the “Law of the Excluded Middle.” It asserts that any proposition is either true or false; there’s no middle ground: \[ {\large \frac{}{~~{\cal A}\lor \lnot {\cal A}~~}}{\small~\mathrm{LEM}} \] Next, we have “Double Negation Elimination.” It asserts that if a proposition \({\cal A}\) can’t be false (i.e., that \(\lnot {\cal A}\) doesn’t hold), then \({\cal A}\) must be true: \[ {\large \frac{~~\lnot\lnot {\cal A}~~}{{\cal A}}}{\small~\mathrm{DNE}} \] (Recall that \(\lnot\lnot {\cal A}\) means \(\lnot(\lnot {\cal A})\).)
As our final classical rule, we have “Indirect Proof.” It asserts that if assuming a proposition is false leads to a contradiction, then the proposition must be true: \[ {\large \frac{~~~\begin{array}{|c} \lnot {\cal A} \\ \hline \vdots \\ \bot \end{array}~~~} {{\cal A}}} {\small~\mathrm{IP}} \] You might wonder, isn’t this just the same as \(\lnot I\) rule we saw above? \[ { \frac{~~~\begin{array}{|c} {\cal A} \\ \hline \vdots \\ \bot \end{array}~~~} {\lnot {\cal A}}} {\small~{\lnot}I} \] The answer is no; unless you already have a rule like DNE or LEM around, showing a proposition can’t be true and concluding that it must be false (\(\lnot I\)) is different from showing that a proposition can’t be false and concluding it’s affirmatively true (IP).
Or to put it another way: if we assume \(\lnot {\cal A}\) and derive a contradiction, the IP rule allows us to conclude \({\cal A}\), but the \(\lnot I\) rule only allows us to conclude that \(\lnot {\cal A}\) doesn’t hold, i.e., that \(\lnot \lnot {\cal A}\) is true.
\(P\to Q \ \ \vdash \ \ \lnot P\lor Q\)
When nothing obvious comes to mind, you can always try the LEM rule for some propositional variable, because then you get extra assumptions that might be helpful in proving your conclusion.
But other approaches work too, e.g.,
\(\vdash\ \ \lnot\lnot P \to P\)
Here it’s pretty obvious which Classical rule will be most helpful.
Previous: 1.8 Natural Deduction Part 1
Next: 2.1 Predicate Logic